'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, half(0(x1)) -> 0(s(s(half(p(s(p(s(x1))))))))
, half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
, rd(0(x1)) -> 0(s(0(0(0(0(s(0(rd(x1)))))))))}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ p^#(0(x1)) -> c_0(p^#(x1))
, p^#(s(x1)) -> c_1()
, p^#(p(s(x1))) -> c_2(p^#(x1))
, f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))
, half^#(0(x1)) -> c_6(half^#(p(s(p(s(x1))))))
, half^#(s(s(x1))) -> c_7(half^#(p(p(s(s(x1))))))
, rd^#(0(x1)) -> c_8(rd^#(x1))}
The usable rules are:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))}
The estimated dependency graph contains the following edges:
{p^#(0(x1)) -> c_0(p^#(x1))}
==> {p^#(p(s(x1))) -> c_2(p^#(x1))}
{p^#(0(x1)) -> c_0(p^#(x1))}
==> {p^#(s(x1)) -> c_1()}
{p^#(0(x1)) -> c_0(p^#(x1))}
==> {p^#(0(x1)) -> c_0(p^#(x1))}
{p^#(p(s(x1))) -> c_2(p^#(x1))}
==> {p^#(p(s(x1))) -> c_2(p^#(x1))}
{p^#(p(s(x1))) -> c_2(p^#(x1))}
==> {p^#(s(x1)) -> c_1()}
{p^#(p(s(x1))) -> c_2(p^#(x1))}
==> {p^#(0(x1)) -> c_0(p^#(x1))}
{f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))}
==> {p^#(s(x1)) -> c_1()}
{g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))}
==> {p^#(p(s(x1))) -> c_2(p^#(x1))}
{g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))}
==> {p^#(s(x1)) -> c_1()}
{g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))}
==> {p^#(0(x1)) -> c_0(p^#(x1))}
{j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))}
==> {p^#(s(x1)) -> c_1()}
{half^#(0(x1)) -> c_6(half^#(p(s(p(s(x1))))))}
==> {half^#(s(s(x1))) -> c_7(half^#(p(p(s(s(x1))))))}
{half^#(0(x1)) -> c_6(half^#(p(s(p(s(x1))))))}
==> {half^#(0(x1)) -> c_6(half^#(p(s(p(s(x1))))))}
{half^#(s(s(x1))) -> c_7(half^#(p(p(s(s(x1))))))}
==> {half^#(s(s(x1))) -> c_7(half^#(p(p(s(s(x1))))))}
{half^#(s(s(x1))) -> c_7(half^#(p(p(s(s(x1))))))}
==> {half^#(0(x1)) -> c_6(half^#(p(s(p(s(x1))))))}
{rd^#(0(x1)) -> c_8(rd^#(x1))}
==> {rd^#(0(x1)) -> c_8(rd^#(x1))}
We consider the following path(s):
1) { g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(0(x1)) -> c_0(p^#(x1))
, p^#(p(s(x1))) -> c_2(p^#(x1))}
The usable rules for this path are the following:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(0(x1)) -> c_0(p^#(x1))
, p^#(p(s(x1))) -> c_2(p^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [1] x1 + [1]
c_1() = [0]
c_2(x1) = [1] x1 + [1]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [1]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p^#(p(s(x1))) -> c_2(p^#(x1))}
and weakly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p^#(p(s(x1))) -> c_2(p^#(x1))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [4]
c_0(x1) = [1] x1 + [1]
c_1() = [0]
c_2(x1) = [1] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [1]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))}
and weakly orienting the rules
{ p^#(p(s(x1))) -> c_2(p^#(x1))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [1] x1 + [2]
c_1() = [0]
c_2(x1) = [1] x1 + [1]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [9]
c_4(x1) = [1] x1 + [1]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
and weakly orienting the rules
{ g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(p(s(x1))) -> c_2(p^#(x1))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [8]
j(x1) = [1] x1 + [1]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [1] x1 + [4]
c_1() = [0]
c_2(x1) = [1] x1 + [1]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [9]
c_4(x1) = [1] x1 + [1]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f(s(x1)) -> p(s(g(p(s(s(x1))))))}
and weakly orienting the rules
{ g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(p(s(x1))) -> c_2(p^#(x1))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f(s(x1)) -> p(s(g(p(s(s(x1))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [13]
g(x1) = [1] x1 + [9]
j(x1) = [1] x1 + [5]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [1] x1 + [3]
c_1() = [0]
c_2(x1) = [1] x1 + [1]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [15]
c_4(x1) = [1] x1 + [1]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p^#(0(x1)) -> c_0(p^#(x1))}
and weakly orienting the rules
{ f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(p(s(x1))) -> c_2(p^#(x1))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p^#(0(x1)) -> c_0(p^#(x1))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [1]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [0]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [1] x1 + [0]
c_1() = [0]
c_2(x1) = [1] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [4]
c_4(x1) = [1] x1 + [1]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))}
Weak Rules:
{ p^#(0(x1)) -> c_0(p^#(x1))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(p(s(x1))) -> c_2(p^#(x1))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))}
Weak Rules:
{ p^#(0(x1)) -> c_0(p^#(x1))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(p(s(x1))) -> c_2(p^#(x1))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
The problem is Match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ p_0(2) -> 10
, p_0(2) -> 12
, p_0(2) -> 25
, p_0(5) -> 4
, p_0(11) -> 10
, p_0(11) -> 25
, p_1(2) -> 16
, p_1(2) -> 22
, p_1(2) -> 24
, p_1(10) -> 22
, p_1(10) -> 24
, p_1(12) -> 22
, p_1(12) -> 24
, p_1(17) -> 8
, p_1(20) -> 19
, p_1(20) -> 21
, p_1(20) -> 44
, p_1(20) -> 46
, p_1(20) -> 66
, p_1(20) -> 68
, p_1(23) -> 22
, p_1(25) -> 22
, p_1(25) -> 24
, p_1(26) -> 25
, p_1(29) -> 28
, p_1(35) -> 34
, p_1(35) -> 50
, p_1(37) -> 34
, p_1(37) -> 36
, p_1(37) -> 50
, p_1(53) -> 52
, p_2(2) -> 47
, p_2(2) -> 49
, p_2(14) -> 41
, p_2(34) -> 47
, p_2(34) -> 49
, p_2(36) -> 47
, p_2(36) -> 49
, p_2(42) -> 32
, p_2(45) -> 44
, p_2(48) -> 47
, p_2(50) -> 47
, p_2(50) -> 49
, p_2(51) -> 50
, p_2(54) -> 19
, p_2(54) -> 21
, p_2(54) -> 44
, p_2(54) -> 46
, p_2(54) -> 66
, p_2(54) -> 68
, p_2(55) -> 54
, p_2(56) -> 19
, p_2(56) -> 21
, p_2(56) -> 44
, p_2(56) -> 46
, p_2(56) -> 66
, p_2(56) -> 68
, p_2(61) -> 60
, p_2(61) -> 72
, p_2(63) -> 60
, p_2(63) -> 62
, p_2(63) -> 72
, p_3(2) -> 69
, p_3(2) -> 71
, p_3(60) -> 69
, p_3(60) -> 71
, p_3(62) -> 69
, p_3(62) -> 71
, p_3(64) -> 58
, p_3(67) -> 66
, p_3(70) -> 69
, p_3(72) -> 69
, p_3(72) -> 71
, p_3(73) -> 72
, 0_0(2) -> 2
, 0_0(2) -> 10
, 0_0(2) -> 12
, 0_0(2) -> 16
, 0_0(2) -> 22
, 0_0(2) -> 24
, 0_0(2) -> 25
, 0_0(2) -> 34
, 0_0(2) -> 36
, 0_0(2) -> 47
, 0_0(2) -> 49
, 0_0(2) -> 50
, 0_0(2) -> 60
, 0_0(2) -> 62
, 0_0(2) -> 69
, 0_0(2) -> 71
, 0_0(2) -> 72
, 0_1(14) -> 10
, 0_1(14) -> 12
, 0_1(14) -> 16
, 0_1(14) -> 22
, 0_1(14) -> 24
, 0_1(14) -> 25
, 0_1(14) -> 47
, 0_1(14) -> 49
, 0_1(14) -> 69
, 0_1(14) -> 71
, 0_2(39) -> 22
, 0_2(39) -> 24
, s_0(2) -> 2
, s_0(2) -> 10
, s_0(2) -> 12
, s_0(2) -> 16
, s_0(2) -> 22
, s_0(2) -> 24
, s_0(2) -> 25
, s_0(2) -> 34
, s_0(2) -> 36
, s_0(2) -> 47
, s_0(2) -> 49
, s_0(2) -> 50
, s_0(2) -> 60
, s_0(2) -> 62
, s_0(2) -> 69
, s_0(2) -> 71
, s_0(2) -> 72
, s_0(6) -> 5
, s_0(7) -> 4
, s_0(7) -> 6
, s_0(8) -> 7
, s_0(10) -> 9
, s_0(12) -> 11
, s_1(2) -> 37
, s_1(2) -> 52
, s_1(10) -> 26
, s_1(15) -> 14
, s_1(16) -> 15
, s_1(16) -> 41
, s_1(18) -> 17
, s_1(19) -> 8
, s_1(19) -> 18
, s_1(21) -> 20
, s_1(24) -> 23
, s_1(30) -> 29
, s_1(31) -> 28
, s_1(31) -> 30
, s_1(32) -> 31
, s_1(34) -> 33
, s_1(36) -> 35
, s_1(37) -> 53
, s_2(2) -> 63
, s_2(34) -> 51
, s_2(40) -> 39
, s_2(41) -> 40
, s_2(43) -> 42
, s_2(44) -> 32
, s_2(44) -> 43
, s_2(46) -> 45
, s_2(49) -> 48
, s_2(56) -> 55
, s_2(57) -> 54
, s_2(57) -> 56
, s_2(58) -> 19
, s_2(58) -> 21
, s_2(58) -> 44
, s_2(58) -> 46
, s_2(58) -> 57
, s_2(58) -> 66
, s_2(58) -> 68
, s_2(60) -> 59
, s_2(62) -> 61
, s_3(60) -> 73
, s_3(65) -> 64
, s_3(66) -> 58
, s_3(66) -> 65
, s_3(68) -> 67
, s_3(71) -> 70
, f_1(22) -> 19
, f_1(22) -> 21
, f_1(22) -> 44
, f_1(22) -> 46
, f_1(22) -> 66
, f_1(22) -> 68
, f_2(47) -> 44
, f_2(47) -> 46
, f_3(69) -> 66
, f_3(69) -> 68
, g_1(52) -> 19
, g_1(52) -> 21
, g_1(52) -> 44
, g_1(52) -> 46
, g_1(52) -> 66
, g_1(52) -> 68
, j_0(9) -> 8
, j_1(33) -> 32
, j_2(59) -> 58
, p^#_0(2) -> 1
, p^#_0(4) -> 3
, p^#_0(6) -> 13
, p^#_1(28) -> 27
, p^#_1(30) -> 38
, c_0_0(1) -> 1
, c_2_0(13) -> 3
, c_2_1(38) -> 27
, g^#_0(2) -> 1
, c_4_0(3) -> 1
, c_4_1(27) -> 1}
2) { g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(0(x1)) -> c_0(p^#(x1))
, p^#(p(s(x1))) -> c_2(p^#(x1))
, p^#(s(x1)) -> c_1()}
The usable rules for this path are the following:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, p^#(0(x1)) -> c_0(p^#(x1))
, p^#(p(s(x1))) -> c_2(p^#(x1))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(s(x1)) -> c_1()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, p^#(s(x1)) -> c_1()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, p^#(s(x1)) -> c_1()}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [3]
c_0(x1) = [1] x1 + [0]
c_1() = [0]
c_2(x1) = [1] x1 + [2]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p^#(p(s(x1))) -> c_2(p^#(x1))}
and weakly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, p^#(s(x1)) -> c_1()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p^#(p(s(x1))) -> c_2(p^#(x1))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [0]
c_1() = [0]
c_2(x1) = [1] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))}
and weakly orienting the rules
{ p^#(p(s(x1))) -> c_2(p^#(x1))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, p^#(s(x1)) -> c_1()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [3]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [0]
c_1() = [0]
c_2(x1) = [1] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [9]
c_4(x1) = [1] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, p^#(0(x1)) -> c_0(p^#(x1))}
and weakly orienting the rules
{ g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(p(s(x1))) -> c_2(p^#(x1))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, p^#(s(x1)) -> c_1()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, p^#(0(x1)) -> c_0(p^#(x1))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [14]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [1] x1 + [0]
c_1() = [0]
c_2(x1) = [1] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
and weakly orienting the rules
{ j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, p^#(0(x1)) -> c_0(p^#(x1))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(p(s(x1))) -> c_2(p^#(x1))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, p^#(s(x1)) -> c_1()}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [1]
g(x1) = [1] x1 + [12]
j(x1) = [1] x1 + [6]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [0]
c_1() = [0]
c_2(x1) = [1] x1 + [1]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [13]
c_4(x1) = [1] x1 + [3]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))}
Weak Rules:
{ g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, p^#(0(x1)) -> c_0(p^#(x1))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(p(s(x1))) -> c_2(p^#(x1))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, p^#(s(x1)) -> c_1()}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))}
Weak Rules:
{ g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, p^#(0(x1)) -> c_0(p^#(x1))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(p(s(x1))) -> c_2(p^#(x1))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, p^#(s(x1)) -> c_1()}
Details:
The problem is Match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ p_0(2) -> 10
, p_0(2) -> 12
, p_0(2) -> 25
, p_0(5) -> 4
, p_0(11) -> 10
, p_0(11) -> 25
, p_1(2) -> 16
, p_1(2) -> 22
, p_1(2) -> 24
, p_1(10) -> 22
, p_1(10) -> 24
, p_1(12) -> 22
, p_1(12) -> 24
, p_1(17) -> 8
, p_1(20) -> 19
, p_1(20) -> 21
, p_1(20) -> 44
, p_1(20) -> 46
, p_1(20) -> 66
, p_1(20) -> 68
, p_1(23) -> 22
, p_1(25) -> 22
, p_1(25) -> 24
, p_1(26) -> 25
, p_1(29) -> 28
, p_1(35) -> 34
, p_1(35) -> 50
, p_1(37) -> 34
, p_1(37) -> 36
, p_1(37) -> 50
, p_1(53) -> 52
, p_2(2) -> 47
, p_2(2) -> 49
, p_2(2) -> 69
, p_2(2) -> 71
, p_2(14) -> 41
, p_2(34) -> 47
, p_2(34) -> 49
, p_2(36) -> 47
, p_2(36) -> 49
, p_2(42) -> 32
, p_2(45) -> 44
, p_2(48) -> 47
, p_2(50) -> 47
, p_2(50) -> 49
, p_2(51) -> 50
, p_2(54) -> 19
, p_2(54) -> 21
, p_2(54) -> 44
, p_2(54) -> 46
, p_2(54) -> 66
, p_2(54) -> 68
, p_2(55) -> 54
, p_2(56) -> 19
, p_2(56) -> 21
, p_2(56) -> 44
, p_2(56) -> 46
, p_2(56) -> 66
, p_2(56) -> 68
, p_2(59) -> 72
, p_2(60) -> 69
, p_2(60) -> 71
, p_2(61) -> 60
, p_2(61) -> 72
, p_2(62) -> 69
, p_2(62) -> 71
, p_2(63) -> 60
, p_2(63) -> 62
, p_2(63) -> 72
, p_2(64) -> 58
, p_2(67) -> 66
, p_2(70) -> 69
, p_2(72) -> 69
, p_2(72) -> 71
, 0_0(2) -> 2
, 0_0(2) -> 10
, 0_0(2) -> 12
, 0_0(2) -> 16
, 0_0(2) -> 22
, 0_0(2) -> 24
, 0_0(2) -> 25
, 0_0(2) -> 34
, 0_0(2) -> 36
, 0_0(2) -> 47
, 0_0(2) -> 49
, 0_0(2) -> 50
, 0_0(2) -> 60
, 0_0(2) -> 62
, 0_0(2) -> 69
, 0_0(2) -> 71
, 0_0(2) -> 72
, 0_1(14) -> 10
, 0_1(14) -> 12
, 0_1(14) -> 16
, 0_1(14) -> 22
, 0_1(14) -> 24
, 0_1(14) -> 25
, 0_1(14) -> 47
, 0_1(14) -> 49
, 0_1(14) -> 69
, 0_1(14) -> 71
, 0_2(39) -> 22
, 0_2(39) -> 24
, s_0(2) -> 2
, s_0(2) -> 10
, s_0(2) -> 12
, s_0(2) -> 16
, s_0(2) -> 22
, s_0(2) -> 24
, s_0(2) -> 25
, s_0(2) -> 34
, s_0(2) -> 36
, s_0(2) -> 47
, s_0(2) -> 49
, s_0(2) -> 50
, s_0(2) -> 60
, s_0(2) -> 62
, s_0(2) -> 69
, s_0(2) -> 71
, s_0(2) -> 72
, s_0(6) -> 5
, s_0(7) -> 4
, s_0(7) -> 6
, s_0(8) -> 7
, s_0(10) -> 9
, s_0(12) -> 11
, s_1(2) -> 37
, s_1(2) -> 52
, s_1(10) -> 26
, s_1(15) -> 14
, s_1(16) -> 15
, s_1(16) -> 41
, s_1(18) -> 17
, s_1(19) -> 8
, s_1(19) -> 18
, s_1(21) -> 20
, s_1(24) -> 23
, s_1(30) -> 29
, s_1(31) -> 28
, s_1(31) -> 30
, s_1(32) -> 31
, s_1(34) -> 33
, s_1(36) -> 35
, s_1(37) -> 53
, s_2(2) -> 63
, s_2(34) -> 51
, s_2(40) -> 39
, s_2(41) -> 40
, s_2(43) -> 42
, s_2(44) -> 32
, s_2(44) -> 43
, s_2(46) -> 45
, s_2(49) -> 48
, s_2(56) -> 55
, s_2(57) -> 54
, s_2(57) -> 56
, s_2(58) -> 19
, s_2(58) -> 21
, s_2(58) -> 44
, s_2(58) -> 46
, s_2(58) -> 57
, s_2(58) -> 66
, s_2(58) -> 68
, s_2(60) -> 59
, s_2(62) -> 61
, s_2(65) -> 64
, s_2(66) -> 58
, s_2(66) -> 65
, s_2(68) -> 67
, s_2(71) -> 70
, f_1(22) -> 19
, f_1(22) -> 21
, f_1(22) -> 44
, f_1(22) -> 46
, f_1(22) -> 66
, f_1(22) -> 68
, f_2(47) -> 44
, f_2(47) -> 46
, f_2(69) -> 66
, f_2(69) -> 68
, g_1(52) -> 19
, g_1(52) -> 21
, g_1(52) -> 44
, g_1(52) -> 46
, g_1(52) -> 66
, g_1(52) -> 68
, j_0(9) -> 8
, j_1(33) -> 32
, j_2(59) -> 58
, p^#_0(2) -> 1
, p^#_0(4) -> 3
, p^#_0(6) -> 13
, p^#_1(28) -> 27
, p^#_1(30) -> 38
, c_0_0(1) -> 1
, c_1_0() -> 1
, c_1_0() -> 3
, c_1_0() -> 13
, c_1_1() -> 27
, c_1_1() -> 38
, c_2_0(13) -> 3
, c_2_1(38) -> 27
, g^#_0(2) -> 1
, c_4_0(3) -> 1
, c_4_1(27) -> 1}
3) { g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(s(x1)) -> c_1()}
The usable rules for this path are the following:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(s(x1)) -> c_1()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [1]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p^#(s(x1)) -> c_1()}
and weakly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p^#(s(x1)) -> c_1()}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [8]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [1]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))}
and weakly orienting the rules
{ p^#(s(x1)) -> c_1()
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [9]
c_4(x1) = [1] x1 + [1]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
and weakly orienting the rules
{ g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(s(x1)) -> c_1()
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [8]
j(x1) = [1] x1 + [1]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [9]
c_4(x1) = [1] x1 + [1]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f(s(x1)) -> p(s(g(p(s(s(x1))))))}
and weakly orienting the rules
{ g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(s(x1)) -> c_1()
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f(s(x1)) -> p(s(g(p(s(s(x1))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [14]
g(x1) = [1] x1 + [11]
j(x1) = [1] x1 + [5]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [13]
c_4(x1) = [1] x1 + [4]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))}
Weak Rules:
{ f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(s(x1)) -> c_1()
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))}
Weak Rules:
{ f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p^#(s(x1)) -> c_1()
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
The problem is Match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ p_0(2) -> 10
, p_0(2) -> 12
, p_0(2) -> 24
, p_0(5) -> 4
, p_0(11) -> 10
, p_0(11) -> 24
, p_1(2) -> 15
, p_1(2) -> 21
, p_1(2) -> 23
, p_1(10) -> 21
, p_1(10) -> 23
, p_1(12) -> 21
, p_1(12) -> 23
, p_1(16) -> 8
, p_1(19) -> 18
, p_1(19) -> 20
, p_1(19) -> 42
, p_1(19) -> 44
, p_1(19) -> 64
, p_1(19) -> 66
, p_1(22) -> 21
, p_1(24) -> 21
, p_1(24) -> 23
, p_1(25) -> 24
, p_1(28) -> 27
, p_1(34) -> 33
, p_1(34) -> 48
, p_1(36) -> 33
, p_1(36) -> 35
, p_1(36) -> 48
, p_1(51) -> 50
, p_2(2) -> 45
, p_2(2) -> 47
, p_2(13) -> 39
, p_2(33) -> 45
, p_2(33) -> 47
, p_2(35) -> 45
, p_2(35) -> 47
, p_2(40) -> 31
, p_2(43) -> 42
, p_2(46) -> 45
, p_2(48) -> 45
, p_2(48) -> 47
, p_2(49) -> 48
, p_2(52) -> 18
, p_2(52) -> 20
, p_2(52) -> 42
, p_2(52) -> 44
, p_2(52) -> 64
, p_2(52) -> 66
, p_2(53) -> 52
, p_2(54) -> 18
, p_2(54) -> 20
, p_2(54) -> 42
, p_2(54) -> 44
, p_2(54) -> 64
, p_2(54) -> 66
, p_2(59) -> 58
, p_2(59) -> 70
, p_2(61) -> 58
, p_2(61) -> 60
, p_2(61) -> 70
, p_3(2) -> 67
, p_3(2) -> 69
, p_3(58) -> 67
, p_3(58) -> 69
, p_3(60) -> 67
, p_3(60) -> 69
, p_3(62) -> 56
, p_3(65) -> 64
, p_3(68) -> 67
, p_3(70) -> 67
, p_3(70) -> 69
, p_3(71) -> 70
, 0_0(2) -> 2
, 0_0(2) -> 10
, 0_0(2) -> 12
, 0_0(2) -> 15
, 0_0(2) -> 21
, 0_0(2) -> 23
, 0_0(2) -> 24
, 0_0(2) -> 33
, 0_0(2) -> 35
, 0_0(2) -> 45
, 0_0(2) -> 47
, 0_0(2) -> 48
, 0_0(2) -> 58
, 0_0(2) -> 60
, 0_0(2) -> 67
, 0_0(2) -> 69
, 0_0(2) -> 70
, 0_1(13) -> 10
, 0_1(13) -> 12
, 0_1(13) -> 15
, 0_1(13) -> 21
, 0_1(13) -> 23
, 0_1(13) -> 24
, 0_1(13) -> 45
, 0_1(13) -> 47
, 0_1(13) -> 67
, 0_1(13) -> 69
, 0_2(37) -> 21
, 0_2(37) -> 23
, s_0(2) -> 2
, s_0(2) -> 10
, s_0(2) -> 12
, s_0(2) -> 15
, s_0(2) -> 21
, s_0(2) -> 23
, s_0(2) -> 24
, s_0(2) -> 33
, s_0(2) -> 35
, s_0(2) -> 45
, s_0(2) -> 47
, s_0(2) -> 48
, s_0(2) -> 58
, s_0(2) -> 60
, s_0(2) -> 67
, s_0(2) -> 69
, s_0(2) -> 70
, s_0(6) -> 5
, s_0(7) -> 4
, s_0(7) -> 6
, s_0(8) -> 7
, s_0(10) -> 9
, s_0(12) -> 11
, s_1(2) -> 36
, s_1(2) -> 50
, s_1(10) -> 25
, s_1(14) -> 13
, s_1(15) -> 14
, s_1(15) -> 39
, s_1(17) -> 16
, s_1(18) -> 8
, s_1(18) -> 17
, s_1(20) -> 19
, s_1(23) -> 22
, s_1(29) -> 28
, s_1(30) -> 27
, s_1(30) -> 29
, s_1(31) -> 30
, s_1(33) -> 32
, s_1(35) -> 34
, s_1(36) -> 51
, s_2(2) -> 61
, s_2(33) -> 49
, s_2(38) -> 37
, s_2(39) -> 38
, s_2(41) -> 40
, s_2(42) -> 31
, s_2(42) -> 41
, s_2(44) -> 43
, s_2(47) -> 46
, s_2(54) -> 53
, s_2(55) -> 52
, s_2(55) -> 54
, s_2(56) -> 18
, s_2(56) -> 20
, s_2(56) -> 42
, s_2(56) -> 44
, s_2(56) -> 55
, s_2(56) -> 64
, s_2(56) -> 66
, s_2(58) -> 57
, s_2(60) -> 59
, s_3(58) -> 71
, s_3(63) -> 62
, s_3(64) -> 56
, s_3(64) -> 63
, s_3(66) -> 65
, s_3(69) -> 68
, f_1(21) -> 18
, f_1(21) -> 20
, f_1(21) -> 42
, f_1(21) -> 44
, f_1(21) -> 64
, f_1(21) -> 66
, f_2(45) -> 42
, f_2(45) -> 44
, f_3(67) -> 64
, f_3(67) -> 66
, g_1(50) -> 18
, g_1(50) -> 20
, g_1(50) -> 42
, g_1(50) -> 44
, g_1(50) -> 64
, g_1(50) -> 66
, j_0(9) -> 8
, j_1(32) -> 31
, j_2(57) -> 56
, p^#_0(2) -> 1
, p^#_0(4) -> 3
, p^#_1(27) -> 26
, c_1_0() -> 1
, c_1_0() -> 3
, c_1_1() -> 26
, g^#_0(2) -> 1
, c_4_0(3) -> 1
, c_4_1(26) -> 1}
4) { j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))
, p^#(s(x1)) -> c_1()}
The usable rules for this path are the following:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))
, p^#(s(x1)) -> c_1()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [1]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [4]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [1]
c_5(x1) = [1] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p^#(s(x1)) -> c_1()}
and weakly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p^#(s(x1)) -> c_1()}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [1]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [2]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [8]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [1]
c_5(x1) = [1] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))}
and weakly orienting the rules
{ p^#(s(x1)) -> c_1()
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [1]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [2]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [9]
c_5(x1) = [1] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))}
and weakly orienting the rules
{ j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))
, p^#(s(x1)) -> c_1()
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [1]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [8]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [9]
c_5(x1) = [1] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
and weakly orienting the rules
{ j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))
, p^#(s(x1)) -> c_1()
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [1]
g(x1) = [1] x1 + [14]
j(x1) = [1] x1 + [8]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [9]
c_5(x1) = [1] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))}
Weak Rules:
{ g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))
, p^#(s(x1)) -> c_1()
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))}
Weak Rules:
{ g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))
, p^#(s(x1)) -> c_1()
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
The problem is Match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ p_0(2) -> 9
, p_0(2) -> 11
, p_0(2) -> 12
, p_0(7) -> 6
, p_0(10) -> 9
, p_0(12) -> 9
, p_0(12) -> 11
, p_1(2) -> 15
, p_1(2) -> 22
, p_1(2) -> 24
, p_1(2) -> 43
, p_1(2) -> 45
, p_1(13) -> 15
, p_1(20) -> 19
, p_1(23) -> 22
, p_1(25) -> 22
, p_1(25) -> 24
, p_1(25) -> 43
, p_1(25) -> 45
, p_1(26) -> 25
, p_1(26) -> 36
, p_1(26) -> 46
, p_1(27) -> 6
, p_1(27) -> 8
, p_1(27) -> 19
, p_1(27) -> 21
, p_1(27) -> 28
, p_1(27) -> 40
, p_1(27) -> 42
, p_1(30) -> 29
, p_1(31) -> 27
, p_1(32) -> 6
, p_1(32) -> 8
, p_1(32) -> 19
, p_1(32) -> 21
, p_1(32) -> 28
, p_1(32) -> 40
, p_1(32) -> 42
, p_1(35) -> 46
, p_1(36) -> 43
, p_1(36) -> 45
, p_1(37) -> 36
, p_1(37) -> 46
, p_1(38) -> 34
, p_1(41) -> 40
, p_1(44) -> 43
, p_1(46) -> 43
, p_1(46) -> 45
, 0_0(2) -> 2
, 0_0(2) -> 9
, 0_0(2) -> 11
, 0_0(2) -> 12
, 0_0(2) -> 15
, 0_0(2) -> 22
, 0_0(2) -> 24
, 0_0(2) -> 25
, 0_0(2) -> 36
, 0_0(2) -> 43
, 0_0(2) -> 45
, 0_0(2) -> 46
, 0_1(13) -> 9
, 0_1(13) -> 11
, 0_1(13) -> 12
, 0_1(13) -> 15
, 0_1(13) -> 22
, 0_1(13) -> 24
, 0_1(15) -> 43
, 0_1(15) -> 45
, s_0(2) -> 2
, s_0(2) -> 9
, s_0(2) -> 11
, s_0(2) -> 12
, s_0(2) -> 15
, s_0(2) -> 22
, s_0(2) -> 24
, s_0(2) -> 25
, s_0(2) -> 36
, s_0(2) -> 43
, s_0(2) -> 45
, s_0(2) -> 46
, s_0(5) -> 4
, s_0(6) -> 5
, s_0(8) -> 7
, s_0(11) -> 10
, s_1(2) -> 26
, s_1(2) -> 29
, s_1(14) -> 13
, s_1(15) -> 14
, s_1(15) -> 15
, s_1(18) -> 17
, s_1(19) -> 18
, s_1(21) -> 20
, s_1(24) -> 23
, s_1(25) -> 37
, s_1(26) -> 30
, s_1(28) -> 27
, s_1(32) -> 31
, s_1(33) -> 27
, s_1(33) -> 32
, s_1(34) -> 6
, s_1(34) -> 8
, s_1(34) -> 19
, s_1(34) -> 21
, s_1(34) -> 28
, s_1(34) -> 33
, s_1(34) -> 40
, s_1(34) -> 42
, s_1(36) -> 35
, s_1(39) -> 38
, s_1(40) -> 34
, s_1(40) -> 39
, s_1(42) -> 41
, s_1(45) -> 44
, f_0(9) -> 6
, f_0(9) -> 8
, f_1(22) -> 19
, f_1(22) -> 21
, f_1(43) -> 40
, f_1(43) -> 42
, g_1(29) -> 6
, g_1(29) -> 8
, g_1(29) -> 19
, g_1(29) -> 21
, g_1(29) -> 28
, g_1(29) -> 40
, g_1(29) -> 42
, j_1(35) -> 34
, p^#_0(2) -> 1
, p^#_0(4) -> 3
, p^#_1(17) -> 16
, c_1_0() -> 1
, c_1_0() -> 3
, c_1_1() -> 16
, j^#_0(2) -> 1
, c_5_0(3) -> 1
, c_5_1(16) -> 1}
5) { f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))
, p^#(s(x1)) -> c_1()}
The usable rules for this path are the following:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))
, p^#(s(x1)) -> c_1()}
Details:
We apply the weight gap principle, strictly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [1]
j(x1) = [1] x1 + [0]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [1]
c_3(x1) = [1] x1 + [1]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{p^#(s(x1)) -> c_1()}
and weakly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{p^#(s(x1)) -> c_1()}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [1]
j(x1) = [1] x1 + [0]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [8]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [1]
c_3(x1) = [1] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))}
and weakly orienting the rules
{ p^#(s(x1)) -> c_1()
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [1]
j(x1) = [1] x1 + [0]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [9]
c_3(x1) = [1] x1 + [1]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f(s(x1)) -> p(s(g(p(s(s(x1))))))}
and weakly orienting the rules
{ f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))
, p^#(s(x1)) -> c_1()
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f(s(x1)) -> p(s(g(p(s(s(x1))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [12]
g(x1) = [1] x1 + [1]
j(x1) = [1] x1 + [0]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [9]
c_3(x1) = [1] x1 + [3]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))}
and weakly orienting the rules
{ f(s(x1)) -> p(s(g(p(s(s(x1))))))
, f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))
, p^#(s(x1)) -> c_1()
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [3]
g(x1) = [1] x1 + [1]
j(x1) = [1] x1 + [12]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [5]
c_3(x1) = [1] x1 + [1]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
Weak Rules:
{ j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))
, p^#(s(x1)) -> c_1()
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
Weak Rules:
{ j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))
, p^#(s(x1)) -> c_1()
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
The problem is Match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ p_0(2) -> 6
, p_1(2) -> 9
, p_1(2) -> 25
, p_1(2) -> 27
, p_1(10) -> 5
, p_1(11) -> 10
, p_1(12) -> 5
, p_1(15) -> 28
, p_1(16) -> 25
, p_1(16) -> 27
, p_1(17) -> 16
, p_1(17) -> 28
, p_1(17) -> 52
, p_1(18) -> 25
, p_1(18) -> 27
, p_1(19) -> 16
, p_1(19) -> 18
, p_1(19) -> 28
, p_1(19) -> 52
, p_1(20) -> 14
, p_1(23) -> 22
, p_1(26) -> 25
, p_1(28) -> 25
, p_1(28) -> 27
, p_1(30) -> 22
, p_1(30) -> 24
, p_1(30) -> 46
, p_1(30) -> 48
, p_1(30) -> 56
, p_1(30) -> 58
, p_1(33) -> 32
, p_2(2) -> 49
, p_2(2) -> 51
, p_2(2) -> 59
, p_2(2) -> 61
, p_2(16) -> 49
, p_2(16) -> 51
, p_2(18) -> 49
, p_2(18) -> 51
, p_2(34) -> 22
, p_2(34) -> 24
, p_2(34) -> 31
, p_2(34) -> 46
, p_2(34) -> 48
, p_2(34) -> 56
, p_2(34) -> 58
, p_2(35) -> 34
, p_2(36) -> 22
, p_2(36) -> 24
, p_2(36) -> 31
, p_2(36) -> 46
, p_2(36) -> 48
, p_2(36) -> 56
, p_2(36) -> 58
, p_2(39) -> 62
, p_2(40) -> 59
, p_2(40) -> 61
, p_2(41) -> 40
, p_2(41) -> 62
, p_2(42) -> 59
, p_2(42) -> 61
, p_2(43) -> 40
, p_2(43) -> 42
, p_2(43) -> 62
, p_2(44) -> 14
, p_2(47) -> 46
, p_2(50) -> 49
, p_2(52) -> 49
, p_2(52) -> 51
, p_2(53) -> 52
, p_2(54) -> 38
, p_2(57) -> 56
, p_2(60) -> 59
, p_2(62) -> 59
, p_2(62) -> 61
, 0_0(2) -> 2
, 0_0(2) -> 6
, 0_0(2) -> 9
, 0_0(2) -> 16
, 0_0(2) -> 18
, 0_0(2) -> 25
, 0_0(2) -> 27
, 0_0(2) -> 28
, 0_0(2) -> 40
, 0_0(2) -> 42
, 0_0(2) -> 49
, 0_0(2) -> 51
, 0_0(2) -> 52
, 0_0(2) -> 59
, 0_0(2) -> 61
, 0_0(2) -> 62
, 0_1(7) -> 6
, 0_1(7) -> 9
, 0_1(7) -> 25
, 0_1(7) -> 27
, 0_1(7) -> 49
, 0_1(7) -> 51
, 0_1(7) -> 59
, 0_1(7) -> 61
, s_0(2) -> 2
, s_0(2) -> 6
, s_0(2) -> 9
, s_0(2) -> 16
, s_0(2) -> 18
, s_0(2) -> 25
, s_0(2) -> 27
, s_0(2) -> 28
, s_0(2) -> 40
, s_0(2) -> 42
, s_0(2) -> 49
, s_0(2) -> 51
, s_0(2) -> 52
, s_0(2) -> 59
, s_0(2) -> 61
, s_0(2) -> 62
, s_0(5) -> 4
, s_1(2) -> 19
, s_1(2) -> 32
, s_1(8) -> 7
, s_1(9) -> 8
, s_1(12) -> 11
, s_1(13) -> 10
, s_1(13) -> 12
, s_1(14) -> 5
, s_1(14) -> 13
, s_1(16) -> 15
, s_1(18) -> 17
, s_1(19) -> 33
, s_1(21) -> 20
, s_1(22) -> 14
, s_1(22) -> 21
, s_1(24) -> 23
, s_1(27) -> 26
, s_1(31) -> 30
, s_2(2) -> 43
, s_2(16) -> 53
, s_2(36) -> 35
, s_2(37) -> 34
, s_2(37) -> 36
, s_2(38) -> 22
, s_2(38) -> 24
, s_2(38) -> 31
, s_2(38) -> 37
, s_2(38) -> 46
, s_2(38) -> 48
, s_2(38) -> 56
, s_2(38) -> 58
, s_2(40) -> 39
, s_2(42) -> 41
, s_2(45) -> 44
, s_2(46) -> 14
, s_2(46) -> 45
, s_2(48) -> 47
, s_2(51) -> 50
, s_2(55) -> 54
, s_2(56) -> 38
, s_2(56) -> 55
, s_2(58) -> 57
, s_2(61) -> 60
, f_1(25) -> 22
, f_1(25) -> 24
, f_2(49) -> 46
, f_2(49) -> 48
, f_2(59) -> 56
, f_2(59) -> 58
, g_0(6) -> 5
, g_1(32) -> 22
, g_1(32) -> 24
, g_1(32) -> 31
, g_1(32) -> 46
, g_1(32) -> 48
, g_1(32) -> 56
, g_1(32) -> 58
, j_1(15) -> 14
, j_2(39) -> 38
, p^#_0(2) -> 1
, p^#_0(4) -> 3
, p^#_1(30) -> 29
, c_1_0() -> 1
, c_1_0() -> 3
, c_1_1() -> 29
, f^#_0(2) -> 1
, c_3_0(3) -> 1
, c_3_1(29) -> 1}
6) {g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))}
The usable rules for this path are the following:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [2]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [1]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))}
and weakly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [1]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [9]
c_4(x1) = [1] x1 + [1]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f(s(x1)) -> p(s(g(p(s(s(x1))))))}
and weakly orienting the rules
{ g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f(s(x1)) -> p(s(g(p(s(s(x1))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [4]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [1]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [5]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [13]
c_4(x1) = [1] x1 + [3]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
and weakly orienting the rules
{ f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [8]
g(x1) = [1] x1 + [6]
j(x1) = [1] x1 + [1]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [1] x1 + [9]
c_4(x1) = [1] x1 + [1]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))}
Weak Rules:
{ g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))}
Weak Rules:
{ g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g^#(s(x1)) -> c_4(p^#(p(s(s(s(j(s(p(s(p(s(x1))))))))))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
The problem is Match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ p_0(2) -> 10
, p_0(2) -> 12
, p_0(2) -> 24
, p_0(5) -> 4
, p_0(11) -> 10
, p_0(11) -> 24
, p_1(2) -> 15
, p_1(2) -> 21
, p_1(2) -> 23
, p_1(10) -> 21
, p_1(10) -> 23
, p_1(12) -> 21
, p_1(12) -> 23
, p_1(16) -> 8
, p_1(19) -> 18
, p_1(19) -> 20
, p_1(19) -> 42
, p_1(19) -> 44
, p_1(19) -> 64
, p_1(19) -> 66
, p_1(22) -> 21
, p_1(24) -> 21
, p_1(24) -> 23
, p_1(25) -> 24
, p_1(28) -> 27
, p_1(34) -> 33
, p_1(34) -> 48
, p_1(36) -> 33
, p_1(36) -> 35
, p_1(36) -> 48
, p_1(51) -> 50
, p_2(2) -> 45
, p_2(2) -> 47
, p_2(13) -> 39
, p_2(33) -> 45
, p_2(33) -> 47
, p_2(35) -> 45
, p_2(35) -> 47
, p_2(40) -> 31
, p_2(43) -> 42
, p_2(46) -> 45
, p_2(48) -> 45
, p_2(48) -> 47
, p_2(49) -> 48
, p_2(52) -> 18
, p_2(52) -> 20
, p_2(52) -> 42
, p_2(52) -> 44
, p_2(52) -> 64
, p_2(52) -> 66
, p_2(53) -> 52
, p_2(54) -> 18
, p_2(54) -> 20
, p_2(54) -> 42
, p_2(54) -> 44
, p_2(54) -> 64
, p_2(54) -> 66
, p_2(59) -> 58
, p_2(59) -> 70
, p_2(61) -> 58
, p_2(61) -> 60
, p_2(61) -> 70
, p_3(2) -> 67
, p_3(2) -> 69
, p_3(58) -> 67
, p_3(58) -> 69
, p_3(60) -> 67
, p_3(60) -> 69
, p_3(62) -> 56
, p_3(65) -> 64
, p_3(68) -> 67
, p_3(70) -> 67
, p_3(70) -> 69
, p_3(71) -> 70
, 0_0(2) -> 2
, 0_0(2) -> 10
, 0_0(2) -> 12
, 0_0(2) -> 15
, 0_0(2) -> 21
, 0_0(2) -> 23
, 0_0(2) -> 24
, 0_0(2) -> 33
, 0_0(2) -> 35
, 0_0(2) -> 45
, 0_0(2) -> 47
, 0_0(2) -> 48
, 0_0(2) -> 58
, 0_0(2) -> 60
, 0_0(2) -> 67
, 0_0(2) -> 69
, 0_0(2) -> 70
, 0_1(13) -> 10
, 0_1(13) -> 12
, 0_1(13) -> 15
, 0_1(13) -> 21
, 0_1(13) -> 23
, 0_1(13) -> 24
, 0_1(13) -> 45
, 0_1(13) -> 47
, 0_1(13) -> 67
, 0_1(13) -> 69
, 0_2(37) -> 21
, 0_2(37) -> 23
, s_0(2) -> 2
, s_0(2) -> 10
, s_0(2) -> 12
, s_0(2) -> 15
, s_0(2) -> 21
, s_0(2) -> 23
, s_0(2) -> 24
, s_0(2) -> 33
, s_0(2) -> 35
, s_0(2) -> 45
, s_0(2) -> 47
, s_0(2) -> 48
, s_0(2) -> 58
, s_0(2) -> 60
, s_0(2) -> 67
, s_0(2) -> 69
, s_0(2) -> 70
, s_0(6) -> 5
, s_0(7) -> 4
, s_0(7) -> 6
, s_0(8) -> 7
, s_0(10) -> 9
, s_0(12) -> 11
, s_1(2) -> 36
, s_1(2) -> 50
, s_1(10) -> 25
, s_1(14) -> 13
, s_1(15) -> 14
, s_1(15) -> 39
, s_1(17) -> 16
, s_1(18) -> 8
, s_1(18) -> 17
, s_1(20) -> 19
, s_1(23) -> 22
, s_1(29) -> 28
, s_1(30) -> 27
, s_1(30) -> 29
, s_1(31) -> 30
, s_1(33) -> 32
, s_1(35) -> 34
, s_1(36) -> 51
, s_2(2) -> 61
, s_2(33) -> 49
, s_2(38) -> 37
, s_2(39) -> 38
, s_2(41) -> 40
, s_2(42) -> 31
, s_2(42) -> 41
, s_2(44) -> 43
, s_2(47) -> 46
, s_2(54) -> 53
, s_2(55) -> 52
, s_2(55) -> 54
, s_2(56) -> 18
, s_2(56) -> 20
, s_2(56) -> 42
, s_2(56) -> 44
, s_2(56) -> 55
, s_2(56) -> 64
, s_2(56) -> 66
, s_2(58) -> 57
, s_2(60) -> 59
, s_3(58) -> 71
, s_3(63) -> 62
, s_3(64) -> 56
, s_3(64) -> 63
, s_3(66) -> 65
, s_3(69) -> 68
, f_1(21) -> 18
, f_1(21) -> 20
, f_1(21) -> 42
, f_1(21) -> 44
, f_1(21) -> 64
, f_1(21) -> 66
, f_2(45) -> 42
, f_2(45) -> 44
, f_3(67) -> 64
, f_3(67) -> 66
, g_1(50) -> 18
, g_1(50) -> 20
, g_1(50) -> 42
, g_1(50) -> 44
, g_1(50) -> 64
, g_1(50) -> 66
, j_0(9) -> 8
, j_1(32) -> 31
, j_2(57) -> 56
, p^#_0(2) -> 1
, p^#_0(4) -> 3
, p^#_1(27) -> 26
, g^#_0(2) -> 1
, c_4_0(3) -> 1
, c_4_1(26) -> 1}
7) {j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))}
The usable rules for this path are the following:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [1]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [0]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [1]
c_5(x1) = [1] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))}
and weakly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [0]
j(x1) = [1] x1 + [0]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [9]
c_5(x1) = [1] x1 + [1]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
and weakly orienting the rules
{ j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [1]
g(x1) = [1] x1 + [7]
j(x1) = [1] x1 + [0]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [5]
c_5(x1) = [1] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))}
and weakly orienting the rules
{ g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [1]
g(x1) = [1] x1 + [11]
j(x1) = [1] x1 + [7]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [1] x1 + [9]
c_5(x1) = [1] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))}
Weak Rules:
{ j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))}
Weak Rules:
{ j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j^#(s(x1)) -> c_5(p^#(s(s(p(s(f(p(s(p(p(s(x1))))))))))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
The problem is Match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ p_0(2) -> 9
, p_0(2) -> 11
, p_0(2) -> 12
, p_0(7) -> 6
, p_0(10) -> 9
, p_0(12) -> 9
, p_0(12) -> 11
, p_1(2) -> 15
, p_1(2) -> 22
, p_1(2) -> 24
, p_1(2) -> 43
, p_1(2) -> 45
, p_1(13) -> 15
, p_1(20) -> 19
, p_1(23) -> 22
, p_1(25) -> 22
, p_1(25) -> 24
, p_1(25) -> 43
, p_1(25) -> 45
, p_1(26) -> 25
, p_1(26) -> 36
, p_1(26) -> 46
, p_1(27) -> 6
, p_1(27) -> 8
, p_1(27) -> 19
, p_1(27) -> 21
, p_1(27) -> 28
, p_1(27) -> 40
, p_1(27) -> 42
, p_1(30) -> 29
, p_1(31) -> 27
, p_1(32) -> 6
, p_1(32) -> 8
, p_1(32) -> 19
, p_1(32) -> 21
, p_1(32) -> 28
, p_1(32) -> 40
, p_1(32) -> 42
, p_1(35) -> 46
, p_1(36) -> 43
, p_1(36) -> 45
, p_1(37) -> 36
, p_1(37) -> 46
, p_1(38) -> 34
, p_1(41) -> 40
, p_1(44) -> 43
, p_1(46) -> 43
, p_1(46) -> 45
, 0_0(2) -> 2
, 0_0(2) -> 9
, 0_0(2) -> 11
, 0_0(2) -> 12
, 0_0(2) -> 15
, 0_0(2) -> 22
, 0_0(2) -> 24
, 0_0(2) -> 25
, 0_0(2) -> 36
, 0_0(2) -> 43
, 0_0(2) -> 45
, 0_0(2) -> 46
, 0_1(13) -> 9
, 0_1(13) -> 11
, 0_1(13) -> 12
, 0_1(13) -> 15
, 0_1(13) -> 22
, 0_1(13) -> 24
, 0_1(15) -> 43
, 0_1(15) -> 45
, s_0(2) -> 2
, s_0(2) -> 9
, s_0(2) -> 11
, s_0(2) -> 12
, s_0(2) -> 15
, s_0(2) -> 22
, s_0(2) -> 24
, s_0(2) -> 25
, s_0(2) -> 36
, s_0(2) -> 43
, s_0(2) -> 45
, s_0(2) -> 46
, s_0(5) -> 4
, s_0(6) -> 5
, s_0(8) -> 7
, s_0(11) -> 10
, s_1(2) -> 26
, s_1(2) -> 29
, s_1(14) -> 13
, s_1(15) -> 14
, s_1(15) -> 15
, s_1(18) -> 17
, s_1(19) -> 18
, s_1(21) -> 20
, s_1(24) -> 23
, s_1(25) -> 37
, s_1(26) -> 30
, s_1(28) -> 27
, s_1(32) -> 31
, s_1(33) -> 27
, s_1(33) -> 32
, s_1(34) -> 6
, s_1(34) -> 8
, s_1(34) -> 19
, s_1(34) -> 21
, s_1(34) -> 28
, s_1(34) -> 33
, s_1(34) -> 40
, s_1(34) -> 42
, s_1(36) -> 35
, s_1(39) -> 38
, s_1(40) -> 34
, s_1(40) -> 39
, s_1(42) -> 41
, s_1(45) -> 44
, f_0(9) -> 6
, f_0(9) -> 8
, f_1(22) -> 19
, f_1(22) -> 21
, f_1(43) -> 40
, f_1(43) -> 42
, g_1(29) -> 6
, g_1(29) -> 8
, g_1(29) -> 19
, g_1(29) -> 21
, g_1(29) -> 28
, g_1(29) -> 40
, g_1(29) -> 42
, j_1(35) -> 34
, p^#_0(2) -> 1
, p^#_0(4) -> 3
, p^#_1(17) -> 16
, j^#_0(2) -> 1
, c_5_0(3) -> 1
, c_5_1(16) -> 1}
8) {f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))}
The usable rules for this path are the following:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
, j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [0]
g(x1) = [1] x1 + [1]
j(x1) = [1] x1 + [2]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [1]
c_3(x1) = [1] x1 + [1]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))}
and weakly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [1]
g(x1) = [1] x1 + [1]
j(x1) = [1] x1 + [0]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [9]
c_3(x1) = [1] x1 + [1]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{f(s(x1)) -> p(s(g(p(s(s(x1))))))}
and weakly orienting the rules
{ f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{f(s(x1)) -> p(s(g(p(s(s(x1))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [8]
g(x1) = [1] x1 + [1]
j(x1) = [1] x1 + [0]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [9]
c_3(x1) = [1] x1 + [1]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))}
and weakly orienting the rules
{ f(s(x1)) -> p(s(g(p(s(s(x1))))))
, f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [1] x1 + [3]
g(x1) = [1] x1 + [1]
j(x1) = [1] x1 + [12]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [1] x1 + [9]
c_3(x1) = [1] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
Weak Rules:
{ j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))}
Weak Rules:
{ j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
, f(s(x1)) -> p(s(g(p(s(s(x1))))))
, f^#(s(x1)) -> c_3(p^#(s(g(p(s(s(x1)))))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
The problem is Match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ p_0(2) -> 6
, p_1(2) -> 9
, p_1(2) -> 25
, p_1(2) -> 27
, p_1(10) -> 5
, p_1(11) -> 10
, p_1(12) -> 5
, p_1(15) -> 28
, p_1(16) -> 25
, p_1(16) -> 27
, p_1(17) -> 16
, p_1(17) -> 28
, p_1(17) -> 52
, p_1(18) -> 25
, p_1(18) -> 27
, p_1(19) -> 16
, p_1(19) -> 18
, p_1(19) -> 28
, p_1(19) -> 52
, p_1(20) -> 14
, p_1(23) -> 22
, p_1(26) -> 25
, p_1(28) -> 25
, p_1(28) -> 27
, p_1(30) -> 22
, p_1(30) -> 24
, p_1(30) -> 46
, p_1(30) -> 48
, p_1(30) -> 56
, p_1(30) -> 58
, p_1(33) -> 32
, p_2(2) -> 49
, p_2(2) -> 51
, p_2(2) -> 59
, p_2(2) -> 61
, p_2(16) -> 49
, p_2(16) -> 51
, p_2(18) -> 49
, p_2(18) -> 51
, p_2(34) -> 22
, p_2(34) -> 24
, p_2(34) -> 31
, p_2(34) -> 46
, p_2(34) -> 48
, p_2(34) -> 56
, p_2(34) -> 58
, p_2(35) -> 34
, p_2(36) -> 22
, p_2(36) -> 24
, p_2(36) -> 31
, p_2(36) -> 46
, p_2(36) -> 48
, p_2(36) -> 56
, p_2(36) -> 58
, p_2(39) -> 62
, p_2(40) -> 59
, p_2(40) -> 61
, p_2(41) -> 40
, p_2(41) -> 62
, p_2(42) -> 59
, p_2(42) -> 61
, p_2(43) -> 40
, p_2(43) -> 42
, p_2(43) -> 62
, p_2(44) -> 14
, p_2(47) -> 46
, p_2(50) -> 49
, p_2(52) -> 49
, p_2(52) -> 51
, p_2(53) -> 52
, p_2(54) -> 38
, p_2(57) -> 56
, p_2(60) -> 59
, p_2(62) -> 59
, p_2(62) -> 61
, 0_0(2) -> 2
, 0_0(2) -> 6
, 0_0(2) -> 9
, 0_0(2) -> 16
, 0_0(2) -> 18
, 0_0(2) -> 25
, 0_0(2) -> 27
, 0_0(2) -> 28
, 0_0(2) -> 40
, 0_0(2) -> 42
, 0_0(2) -> 49
, 0_0(2) -> 51
, 0_0(2) -> 52
, 0_0(2) -> 59
, 0_0(2) -> 61
, 0_0(2) -> 62
, 0_1(7) -> 6
, 0_1(7) -> 9
, 0_1(7) -> 25
, 0_1(7) -> 27
, 0_1(7) -> 49
, 0_1(7) -> 51
, 0_1(7) -> 59
, 0_1(7) -> 61
, s_0(2) -> 2
, s_0(2) -> 6
, s_0(2) -> 9
, s_0(2) -> 16
, s_0(2) -> 18
, s_0(2) -> 25
, s_0(2) -> 27
, s_0(2) -> 28
, s_0(2) -> 40
, s_0(2) -> 42
, s_0(2) -> 49
, s_0(2) -> 51
, s_0(2) -> 52
, s_0(2) -> 59
, s_0(2) -> 61
, s_0(2) -> 62
, s_0(5) -> 4
, s_1(2) -> 19
, s_1(2) -> 32
, s_1(8) -> 7
, s_1(9) -> 8
, s_1(12) -> 11
, s_1(13) -> 10
, s_1(13) -> 12
, s_1(14) -> 5
, s_1(14) -> 13
, s_1(16) -> 15
, s_1(18) -> 17
, s_1(19) -> 33
, s_1(21) -> 20
, s_1(22) -> 14
, s_1(22) -> 21
, s_1(24) -> 23
, s_1(27) -> 26
, s_1(31) -> 30
, s_2(2) -> 43
, s_2(16) -> 53
, s_2(36) -> 35
, s_2(37) -> 34
, s_2(37) -> 36
, s_2(38) -> 22
, s_2(38) -> 24
, s_2(38) -> 31
, s_2(38) -> 37
, s_2(38) -> 46
, s_2(38) -> 48
, s_2(38) -> 56
, s_2(38) -> 58
, s_2(40) -> 39
, s_2(42) -> 41
, s_2(45) -> 44
, s_2(46) -> 14
, s_2(46) -> 45
, s_2(48) -> 47
, s_2(51) -> 50
, s_2(55) -> 54
, s_2(56) -> 38
, s_2(56) -> 55
, s_2(58) -> 57
, s_2(61) -> 60
, f_1(25) -> 22
, f_1(25) -> 24
, f_2(49) -> 46
, f_2(49) -> 48
, f_2(59) -> 56
, f_2(59) -> 58
, g_0(6) -> 5
, g_1(32) -> 22
, g_1(32) -> 24
, g_1(32) -> 31
, g_1(32) -> 46
, g_1(32) -> 48
, g_1(32) -> 56
, g_1(32) -> 58
, j_1(15) -> 14
, j_2(39) -> 38
, p^#_0(2) -> 1
, p^#_0(4) -> 3
, p^#_1(30) -> 29
, f^#_0(2) -> 1
, c_3_0(3) -> 1
, c_3_1(29) -> 1}
9) { half^#(0(x1)) -> c_6(half^#(p(s(p(s(x1))))))
, half^#(s(s(x1))) -> c_7(half^#(p(p(s(s(x1))))))}
The usable rules for this path are the following:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)
, half^#(0(x1)) -> c_6(half^#(p(s(p(s(x1))))))
, half^#(s(s(x1))) -> c_7(half^#(p(p(s(s(x1))))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
s(x1) = [1] x1 + [0]
f(x1) = [0] x1 + [0]
g(x1) = [0] x1 + [0]
j(x1) = [0] x1 + [0]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [1] x1 + [3]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [1] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{half^#(0(x1)) -> c_6(half^#(p(s(p(s(x1))))))}
and weakly orienting the rules
{ p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{half^#(0(x1)) -> c_6(half^#(p(s(p(s(x1))))))}
Details:
Interpretation Functions:
p(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [1]
s(x1) = [1] x1 + [0]
f(x1) = [0] x1 + [0]
g(x1) = [0] x1 + [0]
j(x1) = [0] x1 + [0]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [1] x1 + [1]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, half^#(s(s(x1))) -> c_7(half^#(p(p(s(s(x1))))))}
Weak Rules:
{ half^#(0(x1)) -> c_6(half^#(p(s(p(s(x1))))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ p(0(x1)) -> 0(s(s(p(x1))))
, half^#(s(s(x1))) -> c_7(half^#(p(p(s(s(x1))))))}
Weak Rules:
{ half^#(0(x1)) -> c_6(half^#(p(s(p(s(x1))))))
, p(s(x1)) -> x1
, p(p(s(x1))) -> p(x1)}
Details:
The problem is Match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ p_0(3) -> 21
, p_0(3) -> 23
, p_0(22) -> 21
, p_1(26) -> 25
, p_1(27) -> 26
, p_1(28) -> 25
, p_1(28) -> 30
, p_1(28) -> 32
, p_1(31) -> 30
, 0_0(2) -> 2
, 0_0(2) -> 21
, 0_0(2) -> 23
, 0_0(2) -> 25
, 0_0(2) -> 30
, 0_0(2) -> 32
, 0_0(3) -> 2
, 0_0(3) -> 21
, 0_0(3) -> 23
, 0_0(3) -> 25
, 0_0(3) -> 30
, 0_0(3) -> 32
, s_0(2) -> 3
, s_0(2) -> 21
, s_0(2) -> 23
, s_0(2) -> 25
, s_0(2) -> 30
, s_0(2) -> 32
, s_0(3) -> 3
, s_0(3) -> 21
, s_0(3) -> 23
, s_0(3) -> 25
, s_0(3) -> 30
, s_0(3) -> 32
, s_0(23) -> 22
, s_1(2) -> 26
, s_1(2) -> 28
, s_1(3) -> 26
, s_1(3) -> 28
, s_1(28) -> 27
, s_1(32) -> 31
, half^#_0(2) -> 19
, half^#_0(3) -> 19
, half^#_0(21) -> 20
, half^#_1(25) -> 24
, half^#_1(30) -> 29
, c_6_0(20) -> 19
, c_6_1(29) -> 19
, c_6_1(29) -> 20
, c_6_1(29) -> 24
, c_6_1(29) -> 29
, c_7_1(24) -> 19
, c_7_1(24) -> 20
, c_7_1(24) -> 24
, c_7_1(24) -> 29}
10)
{rd^#(0(x1)) -> c_8(rd^#(x1))}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
p(x1) = [0] x1 + [0]
0(x1) = [0] x1 + [0]
s(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
g(x1) = [0] x1 + [0]
j(x1) = [0] x1 + [0]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {rd^#(0(x1)) -> c_8(rd^#(x1))}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{rd^#(0(x1)) -> c_8(rd^#(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{rd^#(0(x1)) -> c_8(rd^#(x1))}
Details:
Interpretation Functions:
p(x1) = [0] x1 + [0]
0(x1) = [1] x1 + [8]
s(x1) = [0] x1 + [0]
f(x1) = [0] x1 + [0]
g(x1) = [0] x1 + [0]
j(x1) = [0] x1 + [0]
half(x1) = [0] x1 + [0]
rd(x1) = [0] x1 + [0]
p^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
f^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
g^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
j^#(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
half^#(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
rd^#(x1) = [1] x1 + [1]
c_8(x1) = [1] x1 + [3]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {rd^#(0(x1)) -> c_8(rd^#(x1))}
Details:
The given problem does not contain any strict rules